\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it Sys}$:AbsInterface(${\it Cmd}$ List), $e$, ${\it e'}$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ ${\it Sys}$))
\\[0ex]$\Rightarrow$ (${\it e'}$ $<$loc $e$)
\\[0ex]$\Rightarrow$ ($\uparrow$(${\it e'}$ $\in_{b}$ ${\it Sys}$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:E(${\it Sys}$). (${\it e'}$ $<$loc $a$) $\Rightarrow$ ($a$ $<$loc $e$) $\Rightarrow$ (filter(${\it isupdate}$;${\it Sys}$($a$)) = [] $\in$ (${\it Cmd}$ List)))
\\[0ex]$\Rightarrow$ (\=filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; $e$))\+
\\[0ex]=
\\[0ex]filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; ${\it e'}$) @ ${\it Sys}$($e$))
\\[0ex]$\in$ (${\it Cmd}$ List))
\-
\end{tabbing}